ds:x:Id fp Type, da:k:Knd fp Type, i:Id, es:ES.
(x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  da(kind(e))?Top)
 (e1, e2:E, L:event-info(ds;da) List.
 (loc(e1) = i
 ( loc(e2) = i
 ( L = nil
 ( L  es-hist{i:l}(es;e1;e2)
 ( e[e1,e2].L = es-hist{i:l}(es;e1;e)) 

latex

Definitions

t  T, x:A. B(x), E, loc(e), Id, b, P  Q, False, A, WellFnd{i}(A;x,y.R(x;y)), x,y. t(x;y), (e <loc e'), P  Q, P & Q, P  Q, es-hist{i:l}(es;e1;e2), event-info(ds;da), Prop, x. t(x), e[e1,e2].P(e), l1  l2, {T}, Top, kind(e), KindDeq, Knd, f(x)?z, valtype(e), IdDeq, vartype(i;x), ES, a:A fp B(a), e  e' , Dec(P), P  Q, 1of(t), A & B, pred(e), es-info(es;e), first(e), x:A. B(x), Trans x,y:T. E(x;y), True, T, as @ bs

Lemmas

es-interval-eq, squash wf, true wf, es-le-self, es-le-trans, es-pred-le, es-le wf, assert wf, es-first wf, iseg append single, es-info wf, es-le-loc, es-le-pred, es-hist-last, es-le-iff, es-pred wf, es-pred-locl, iseg nil, assert of null, decidable es-locl, es-le-not-locl, decidable es-le, es-interval-is-nil, fpf wf, event system wf, es-vartype wf, id-deq wf, es-valtype wf, fpf-cap wf, Knd wf, Kind-deq wf, es-kind wf, top wf, es-locl-wellfnd, es-locl wf, not wf, iseg wf, existse-between2 wf, event-info wf, es-hist wf, es-loc-pred, wellfounded functionality wrt iff, es-locl-iff, Id wf, es-loc wf, es-E wf